$\forall$$A$:Type, ${\it eq}$:EqDecider($A$), $f$, $g$:$x$:$A$ fp$\rightarrow$ Top.
\\[0ex]fpf{-}is{-}empty($f$ $\oplus$ $g$) $\sim$ (fpf{-}is{-}empty($f$) $\wedge_{2}$ fpf{-}is{-}empty($g$))